In the context of hardware and software systems, software testing has been extensively deployed to debug a system or to demonstrate that a system exhibits some properties. Nonetheless, software testing oftentimes cannot by itself prove that a system does not have a certain type of defect. Nor can it demonstrate, also by itself, that a system exhibits certain properties. On the other hand, formal verification can sufficiently prove or disprove the correctness of a software and hardware system by using mathematical methods and thus prove that the system of interest does not have certain defects or does exhibit certain properties.
More specifically, by using abstract mathematical models, formal verification attempts to prove that the system of interest meets certain requirements or that the system can exhibit certain properties or behaviors. That is, formal verification of such systems is performed by providing a formal proof on an abstract mathematical model of these systems. Some typical examples of mathematical objects often used to model systems are finite state machines and various automata.
There are generally two approaches to the formal verification process. One approach is commonly referred to as model checking. Model checking often comprises of a systematically exhaustive exploration of a finite mathematical model and verifies the system of interest by exploring all states and transitions in the model. Model checking also oftentimes invokes some abstraction techniques to avoid having to consider each individual state in the system so as to reduce computation time.
The other approach is logical inference which comprises of a formal version of mathematical reasoning about the system involving certain theorem proving processes. The items to be verified are often expressed in terms of some form of temporal logics such as linear temporal logic or computational tree logic. The drawback of this latter logical inference approach is that the logical inference approach is usually partially automated, and its efficiency and viability may turn on the user's knowledge about the system of interest.
Due to various limitations and drawbacks of the logical inference approach, model checking has been the widely accepted technique for formally verifying the correctness of hardware and software systems. One of the major hurdles for the wide-applicability of this technique is the state-explosion problem, arising from the increasing complexity of real world systems. Compositional verification is an approach for alleviating the state-explosion problem. The compositional verification decomposes a verification task for the software and hardware system into simpler verification problems for the individual components of the system. For example, consider a system M which is composed of two components M1 and M2, and a property P that needs to be verified on M. The assume-guarantee style for compositional verification uses an inference rule which states: P can be verified on M by identifying an assumption A such that A holds on M1 in all environments and M2 satisfies P in any environment that satisfies A. The key to the successful application of this inference rule is the automatic identification of a compact assumption A.
Conventionally, some prior approaches have proposed a polynomial-time approximation method for computing a separating automaton. These method are based on a modification of Angluin's L* method for active learning of a regular language. Some prior art approaches have presented a symbolic implementation of this L*-based approach. Nonetheless, the primary drawback of this approach is that there is no approximation bound. That is, in the worst case scenario, the L* method will return the trivial solution M1 as the separating language, and thus provide no benefit in terms of state space reduction that could not be obtained by simply minimizing M1. As such, there exists a need for alleviating the impact of state-explosion problem in compositional verification.
Disclosed is a method, system, and computer program product for computing a minimal deterministic finite automaton that separates two languages. In some embodiments of the present invention, the method uses a sampling approach and a Boolean Satisfiability solver. Yet in some embodiments of the present invention, the method may be applied for the generation of an intermediate assertion for formal verification using assume-guarantee reasoning.
Further details of aspects, objects, and advantages of the invention are described below in the detailed description, drawings, and claims. Both the foregoing general description and the following detailed description are exemplary and explanatory, and are not intended to be limiting as to the scope of the invention.